a:Atom1, A:MsgA, k:Knd.
AtomFree(ds(A))
 AtomFree(da(A))
 z,z@0,x. A.ef(k,x,z@0,z)?z@0(x):A.da(k)A.stateA.state>>a
 ma-body(A):Shape(A)>>a 

latex

Definitions

Shape(M), x:T>>a, x:A. B(x), xdom(f). v=f(x)   P(x;v), f(a), x.A(x), nat-deq-aux, <a,b>, NatDeq, atom-deq-aux, AtomDeq, #$n, a<b, Void, False, x:AB(x), P  Q, A, AB, , {x:A| B(x) }, , Atom, prod-deq(A;B;a;b), proddeq(a;b), product-deq(A;B;a;b), IdLnkDeq, x:AB(x), IdLnk, sum-deq(A;B;a;b), sumdeq(a;b), union-deq(A;B;a;b), left+right, EqDecider(T), ds(M), da(M), M.ef(k,x,s,v)?w, Valtype(da;k), M.ds(x), M.da(a), State(ds), M.state, AtomFree(d), Atom$n, KindDeq, Type, Knd, a:A fp B(a), AtomFree(T;x), IdDeq, Id, MsgA, t  T, P  Q, x. t(x), Top, f(x)?z, type List, 2of(t), 1of(t), b, f(x), s = t, b, , Prop, x  dom(f), P & Q, P  Q, Unit, rcv(l,tg), P  Q, locl(a), {T}, A/x,y. B(x;y), *, , inr(x), false, reduce(f;k;as), deq-member(eq;x;L), Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, nth_tl(n;as), nil, Case of a; nil  s ; x.y, rec:z  t(x;y;z), hd(l), l[i], ||as||, A & B, x:A. B(x), (x  l), MsgA(ds;da), ma-body(M)

Lemmas

locl wf, pair-inherence, rcv wf, IdLnk wf, inherence-trivial, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, not wf, assert wf, fpf-ap wf, product-deq wf, fpf-cap-void-subtype, inherence-ap-elim, ma-state wf, pi1 wf, pi2 wf, fpf-cap wf, top wf, fpf wf, msga wf, ma ds wf, atom-free-decl wf, ma da wf, atom-free-ma-state, atom-free-ma-da, inheres wf, ma-st wf, ma-da wf, ma-ef-val wf, id-deq wf, Id wf, atom-free-Id, atom-free-fpf, Kind-deq wf, Knd wf, atom-free-Knd